le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
QUICKSORT(x) → TAIL(x)
QUICKSORT(x) → HEAD(x)
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_QS(false, x, n, y) → APP(quicksort(x), add(n, quicksort(y)))
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
HIGH(n, add(m, x)) → LE(m, n)
LE(s(x), s(y)) → LE(x, y)
LOW(n, add(m, x)) → LE(m, n)
QUICKSORT(x) → HIGH(head(x), tail(x))
APP(add(n, x), y) → APP(x, y)
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
QUICKSORT(x) → LOW(head(x), tail(x))
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_LOW(true, n, add(m, x)) → LOW(n, x)
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)
QUICKSORT(x) → ISEMPTY(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
QUICKSORT(x) → TAIL(x)
QUICKSORT(x) → HEAD(x)
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_QS(false, x, n, y) → APP(quicksort(x), add(n, quicksort(y)))
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
HIGH(n, add(m, x)) → LE(m, n)
LE(s(x), s(y)) → LE(x, y)
LOW(n, add(m, x)) → LE(m, n)
QUICKSORT(x) → HIGH(head(x), tail(x))
APP(add(n, x), y) → APP(x, y)
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
QUICKSORT(x) → LOW(head(x), tail(x))
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_LOW(true, n, add(m, x)) → LOW(n, x)
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)
QUICKSORT(x) → ISEMPTY(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APP(add(n, x), y) → APP(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(add(n, x), y) → APP(x, y)
The value of delta used in the strict ordering is 1/2.
POL(APP(x1, x2)) = (2)x_1
POL(add(x1, x2)) = 1/4 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 85/16.
POL(s(x1)) = 5/4 + (15/4)x_1
POL(LE(x1, x2)) = x_1 + (13/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_HIGH(false, n, add(m, x)) → HIGH(n, x)
HIGH(n, add(m, x)) → IF_HIGH(le(m, n), n, add(m, x))
IF_HIGH(true, n, add(m, x)) → HIGH(n, x)
The value of delta used in the strict ordering is 1/8.
POL(add(x1, x2)) = 1/2 + (4)x_2
POL(le(x1, x2)) = (4)x_1 + (1/4)x_2
POL(true) = 0
POL(IF_HIGH(x1, x2, x3)) = (1/4)x_3
POL(false) = 0
POL(s(x1)) = 4 + (3/2)x_1
POL(HIGH(x1, x2)) = (1/2)x_2
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_LOW(true, n, add(m, x)) → LOW(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_LOW(false, n, add(m, x)) → LOW(n, x)
IF_LOW(true, n, add(m, x)) → LOW(n, x)
Used ordering: Polynomial interpretation [25,35]:
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
The value of delta used in the strict ordering is 1/16.
POL(add(x1, x2)) = 1/4 + (9/4)x_1 + (4)x_2
POL(le(x1, x2)) = 4 + (15/4)x_1 + (13/4)x_2
POL(true) = 7/2
POL(false) = 2
POL(s(x1)) = 5/2
POL(LOW(x1, x2)) = (5/4)x_1 + (1/4)x_2
POL(IF_LOW(x1, x2, x3)) = (5/4)x_2 + (1/4)x_3
POL(0) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
LOW(n, add(m, x)) → IF_LOW(le(m, n), n, add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
IF_QS(false, x, n, y) → QUICKSORT(x)
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
IF_QS(false, x, n, y) → QUICKSORT(y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_QS(false, x, n, y) → QUICKSORT(x)
IF_QS(false, x, n, y) → QUICKSORT(y)
Used ordering: Polynomial interpretation [25,35]:
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
The value of delta used in the strict ordering is 1/16.
POL(tail(x1)) = (1/4)x_1
POL(high(x1, x2)) = x_2
POL(le(x1, x2)) = 0
POL(isempty(x1)) = (1/4)x_1
POL(head(x1)) = 0
POL(true) = 0
POL(QUICKSORT(x1)) = (1/4)x_1
POL(0) = 2
POL(IF_QS(x1, x2, x3, x4)) = (1/4)x_1 + (1/4)x_2 + (1/2)x_4
POL(add(x1, x2)) = 1 + (4)x_2
POL(if_high(x1, x2, x3)) = x_3
POL(low(x1, x2)) = x_2
POL(false) = 1/4
POL(s(x1)) = 7/4 + (4)x_1
POL(nil) = 0
POL(if_low(x1, x2, x3)) = x_3
tail(add(n, x)) → x
isempty(nil) → true
if_high(false, n, add(m, x)) → add(m, high(n, x))
isempty(add(n, x)) → false
low(n, nil) → nil
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
high(n, nil) → nil
if_high(true, n, add(m, x)) → high(n, x)
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
QUICKSORT(x) → IF_QS(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_low(false, n, add(m, x)) → low(n, x)
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))
head(add(n, x)) → n
tail(add(n, x)) → x
isempty(nil) → true
isempty(add(n, x)) → false
quicksort(x) → if_qs(isempty(x), low(head(x), tail(x)), head(x), high(head(x), tail(x)))
if_qs(true, x, n, y) → nil
if_qs(false, x, n, y) → app(quicksort(x), add(n, quicksort(y)))